#ifndef TEACHER_H
#define TEACHER_H
#include "cdnf.h"
#include "model.h"
#include "valuation.h"
namespace cdnf {

class Teacher {
public:
	Teacher(Model& model);
	~Teacher();
	bool isEqual(CDNF& cdnf);
	bool isMembership(Valuation& valuation);
	Valuation& getCounterexample();
	void addErrorPoint(Valuation& valuation);
	void reduceCubeByUNSat(Valuation& valuation, bool* inputs);
	std::vector<int> reduceCubeBySim(Valuation& pre, Valuation& post, bool* inputs);	
	bool isConflict();
	int sizeOfError();
	bool failed;
	bool flag;
	std::vector<int> cterms;
	clock_t time_eq,time_mq,time_check,time_red;
	int num_mem, num_eq, num_add, num_remove, num_init;
private:
	Valuation counterExample;
	Model model;
	DNF errorSet;
	bool withinI(Valuation& valuation);
	bool withinNotP(Valuation& valuation);
	void coreOfUnsat(Minisat::Solver& solver,Valuation& valuation,bool* inputs,
			std::vector<int>& indexList);
	void addErrorPoints(const std::vector<int>& terms);	
	void constructII(CDNF& cdnf,Minisat::Solver& solver, bool flag, int offset);
	void generalize(CDNF& cdnf, Valuation& valuation);
};

}
#endif
